pnueli-zuck.5.jani:model: info: pnueli-zuck.5 is an MDP model.
pnueli-zuck.5.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.5.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.5.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.5.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.5.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.5.jani: info: Need 16 bytes per state.
pnueli-zuck.5.jani: info: Explored 307523 states.
Peak memory usage: 239 MB
Analysis results for pnueli-zuck.5.jani
+ State space exploration
State size: 16 bytes
States: 307523
Transitions: 1753715
Branches: 1886851
Rate: 191962 states/s
Time: 1.7 s
+ Property live
Probability: 1
Time: 0.7 s
+ Precomputations
Max. prob. 0 states: 0
Time for max. prob. 0 states: 0.1 s
Max. prob. 1 states: 307523
Time for max. prob. 1 states: 0.6 s
Exported results to file "/out.txt".